package com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation;

import com.googlecode.kipler.syntax.LTLUnaryOperator;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.LTLUnaryFormula;


public class AlwaysAlphaFormula implements AlphaFormula {

	private LTLUnaryFormula unFor;

	private Formula alpha1, alpha2;

	private boolean valid;

	public AlwaysAlphaFormula() {
		super();
	}

	public AlwaysAlphaFormula(Formula f) {
		setAlpha(f);
	}

	@Override
	public void setAlpha(Formula f) {
		valid = false;
		if (f instanceof LTLUnaryFormula) {
			unFor = (LTLUnaryFormula) f;
			if (unFor.getConstructor() == LTLUnaryOperator.ALWAYS) {
				alpha1 = unFor.getOperand();
				alpha2 = new LTLUnaryFormula(LTLUnaryOperator.NEXT, unFor);
				valid = true;
			}
		}
	}

	@Override
	public Formula getAlpha1() {
		return alpha1;
	}

	@Override
	public Formula getAlpha2() {
		return alpha2;
	}

	public boolean isValid() {
		return valid;
	}

}
